Scholia DSH 插件
Scholia 是一款針對 Lean 4 / Mathlib 的插件，旨在解決定理依賴錐（可能多達 1829 個模塊）閱讀困難的問題。它通過算法將複雜的依賴關係簡化爲一條可讀的主線，並將定理渲染爲論文風格頁面。 該插件支持生成包含數學公式、源碼、分步標註、閱讀大綱、步驟頁面以及模塊級依賴圖（DAG）的靜態頁面。目前版本爲 v0.1，依賴 Node.js 24+ 和 SQLite，需配合外部 Corpus 數據使用。
閱讀全文dsh-tool-strict-check: 用真實編譯器校驗代碼與命令
`dsh-tool-strict-check` 是一個用於 DeepSeek Harness (DSH) 的主機插件，旨在通過引入真實的編譯器檢查器（如 Lean 4 內核、Shell 危險規則）來替代智能體主觀判斷，從而修復其機械性錯誤。 該插件位於 `admin-security` 類別，提供四種檢查模式：`status`、`lean`（運行 Lean 4 並禁止 `sorry`）、`batch`（編譯器語法檢查）和 `commands`（Shell 靜態規則）。安裝需將插件添加至 DSH profile，並按需安裝 Lean 4 工具鏈。它通過強制執行嚴格的編譯規則來驗證代碼，但不支持
閱讀全文